ASPMT(QS): Non-Monotonic Spatial Reasoning with Answer Set Programming Modulo Theories

摘要

The systematic modelling of \emph{dynamic spatial systems} [9] is a keyrequirement in a wide range of application areas such as comonsense cognitiverobotics, computer-aided architecture design, dynamic geographic informationsystems. We present ASPMT(QS), a novel approach and fully-implemented prototypefor non-monotonic spatial reasoning ---a crucial requirement within dynamicspatial systems-- based on Answer Set Programming Modulo Theories (ASPMT).ASPMT(QS) consists of a (qualitative) spatial representation module (QS) and amethod for turning tight ASPMT instances into Sat Modulo Theories (SMT)instances in order to compute stable models by means of SMT solvers. Weformalise and implement concepts of default spatial reasoning and spatial frameaxioms using choice formulas. Spatial reasoning is performed by encodingspatial relations as systems of polynomial constraints, and solving via SMTwith the theory of real nonlinear arithmetic. We empirically evaluate ASPMT(QS)in comparison with other prominent contemporary spatial reasoning systems. Ourresults show that ASPMT(QS) is the only existing system that is capable ofreasoning about indirect spatial effects (i.e. addressing the ramificationproblem), and integrating geometric and qualitative spatial information withina non-monotonic spatial reasoning context.